H ? « ‹ ← → › »

Language peer sets for Edinburgh LCF:
United Kingdom↑
United Kingdom/1979↑
Designed 1979 ↑
1970s languages ↑
Fourth generation↑
High Cold War↑

Edinburgh LCF(ID:8177/)

alternate simple view
Country: United Kingdom
Designed 1979

Milner's "mechanisation" of Scott's LCF, which was (quoting the Turing Award citation), "probably the first theoretically based yet practical tool for machine-assisted proof construction."

There are two kinds of base variables and constants in LCF. Those that range over individuals
and those that range over truth values.
Related languages
LCF → Edinburgh LCF   Implementation of
Edinburgh LCF → Cambridge LCF   Evolution of
Edinburgh LCF → ML   Meta language for
Edinburgh LCF → PCF   Implementation
References:
  • Gordon, M.; Milner, R.; Wadsworth, C. (1979) Gordon, M.; Milner, R.; Wadsworth, C. "Edinburgh LCF: a mechanised logic of computation" LNCS 78 Springer-Verlag, 1979
  • Jacek Leszczylowski (1980) Jacek Leszczylowski "An Experiment with Edinburgh LCF", 5th Conference on Automated Deduction, Les Arcs, France, LNCS 87, 1980
  • Leszczylowski, Jacek (1980) Leszczylowski, Jacek "Edinburgh LCF Supporting FP-Systems", Springer, IFB 33, 1980
  • Leszczylowski, Jacek (1980) Leszczylowski, Jacek "On Proving Laws of the Algebra of FP-Systems in Edinburgh LCF", First Annual National Conference on Artificial Intelligence, Stanford, 1980
  • Leszczylowski, Jacek (1980) Leszczylowski, Jacek "Theory of FP-systems in Edinburgh LCF", Computer Science Department,Technical Reports, Edinburgh, Scotland, 1980
  • Leszczylowski, Jacek and I.Hansen (1980) Leszczylowski, Jacek and I.Hansen "Models of Microprograms", Proc. 13th Annual Workshop on Microprogramming, Colorado Springs, USA 1980
  • Leszczylowski, Jacek (1981) Leszczylowski, Jacek "FP-systems in Edinburgh LCF", Proc. of the International Colloquium on Formalization of Programming Concepts, Peniscola, Spain, LNCS 107, 1981
  • Cohn, A. (1982) Cohn, A. "The correctness of a predecence parsing algorithm in LCF." Technical Report No. 21, University of Cambridge, 1982.
  • Cohn, A. and Milner, R. (1982) Cohn, A. and Milner, R. "On using Edinburgh LCF to prove the correctness of a parsing algorithm." Technical Report CSR-113-82, University of Edinburgh, 1982
  • Cohn, Avra; Milner, Robin (1982) Cohn, Avra; Milner, Robin "On using Edinburgh LCF to prove the correctness of a parsing algorithm" Technical Report UCAM-CL-TR-20 February 1982 Online copy at UCAM
  • Cohn, A. (1983) Cohn, A. "The Equivalence of Two Semantic Definitions: A Case Study in LCF." SIAM Journal of Computing. May 1983.
    Search in: Google  Google scholar  World Cat  Yahoo  Overture  DBLP  Monash bib  NZ  IEEE  ACM portal  CiteSeer  CSB  ncstrl  jstor  Bookfinder